; EXPECT: sat
(set-logic QF_UFNIA)
(declare-fun o (Int) Int)
(declare-fun i (Int Int Int) Int)
(define-fun b () Int 2)
(define-fun n ((o Int) (a Int) (b Int)) Int (ite (= b 0) a (mod a b)))
(define-fun p () Bool (= 0 (o 3)))
(declare-fun k () Int)
(declare-fun m (Int Int) Int)
(assert (> k 0))
(assert (and (= 1 (o 0)) (= 2 (o 1)) (= 4 (o 2)) (= 8 (o 3))))
(declare-fun C () Int)
(assert (and (>= C 0) (<= C (- (o k) 1))))
(declare-fun j () Int)
(assert (and (>= j 0) (<= j (- (o k) 1))))
(assert (distinct (i 0 (o k) (ite (= 0 (o k)) (+ C (ite (= 0 (o k)) (- (o k) j) (mod (- (o k) j) (o k)))) (mod (+ C (ite (= 0 (o k)) (- (o k) j) (mod (- (o k) j) (o k)))) (o k)))) (ite (= 0 (o k)) (+ j (ite (= 0 (o k)) (+ (- (o k) 1) (ite (= 0 (o k)) (- (o k) C) (mod (- (o k) C) (o k)))) (mod (+ (- (o k) 1) (ite (= 0 (o k)) (- (o k) C) (mod (- (o k) C) (o k)))) (o k)))) (mod (+ j (ite (= 0 (o k)) (+ (- (o k) 1) (ite (= 0 (o k)) (- (o k) C) (mod (- (o k) C) (o k)))) (mod (+ (- (o k) 1) (ite (= 0 (o k)) (- (o (* j (m 0 (n 0 0 (o C))))) C) (mod (- (o k) C) (o k)))) (o k)))) (o k)))))
(check-sat)
